To address the increasing design complexity and size associated with contemporary software systems, it is generally recognized that new or improved software verification methodologies would represent a significant advance in the art. Accordingly, we describe such methods and techniques which advance high-level bounded model checking (BMC) and high-level synthesis as applied to verification.